\begin{tabbing}
es{-}update{-}iff(${\it es}$;$i$;$x$;${\it ds}$;$e$.$P$($e$);$s$.$f$($s$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. es{-}vartype(${\it es}$; $i$; $x$) $\subseteq$r fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))\+
\\[0ex]c$\wedge$ \=alle{-}at(${\it es}$;$i$;$e$.(\=$P$($e$)\+\+
\\[0ex]$\Rightarrow$ (\=es{-}after(${\it es}$; $x$; $e$)\+
\\[0ex]=
\\[0ex]$f$(es{-}state{-}when(${\it es}$;$e$))
\\[0ex]$\in$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top)))
\-\-\\[0ex]\& (($\neg$$P$($e$)) $\Rightarrow$ (es{-}after(${\it es}$; $x$; $e$) = es{-}when(${\it es}$; $x$; $e$) $\in$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))))
\-\-
\end{tabbing}